1  /-
  2  Copyright (c) 2019 Scott Morrison. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Scott Morrison
  5  -/
  6  import algebra.category.CommRing.basic
src         └─────────────────────────────┘
  7  import category_theory.limits.limits
src         └───────────────────────────┘
  8  
  9  /-!
 10  # The category of commutative rings has all colimits.
 11  
 12  This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
 13  It is a very uniform approach, that conceivably could be synthesised directly
 14  by a tactic that analyses the shape of `comm_ring` and `ring_hom`.
 15  -/
 16  
 17  universes u v
 18  
 19  open category_theory
 20  open category_theory.limits
 21  
 22  -- [ROBOT VOICE]:
 23  -- You should pretend for now that this file was automatically generated.
 24  -- It follows the same template as colimits in Mon.
 25  -- Note that this means this file does not meet documentation standards.
 26  /-
 27  `#print comm_ring` says:
 28  
 29  structure comm_ring : Type u → Type u
 30  fields:
 31  comm_ring.zero : Π (α : Type u) [c : comm_ring α], α
 32  comm_ring.one : Π (α : Type u) [c : comm_ring α], α
 33  comm_ring.neg : Π {α : Type u} [c : comm_ring α], α → α
 34  comm_ring.add : Π {α : Type u} [c : comm_ring α], α → α → α
 35  comm_ring.mul : Π {α : Type u} [c : comm_ring α], α → α → α
 36  
 37  comm_ring.zero_add : ∀ {α : Type u} [c : comm_ring α] (a : α), 0 + a = a
 38  comm_ring.add_zero : ∀ {α : Type u} [c : comm_ring α] (a : α), a + 0 = a
 39  comm_ring.one_mul : ∀ {α : Type u} [c : comm_ring α] (a : α), 1 * a = a
 40  comm_ring.mul_one : ∀ {α : Type u} [c : comm_ring α] (a : α), a * 1 = a
 41  comm_ring.add_left_neg : ∀ {α : Type u} [c : comm_ring α] (a : α), -a + a = 0
 42  comm_ring.add_comm : ∀ {α : Type u} [c : comm_ring α] (a b : α), a + b = b + a
 43  comm_ring.mul_comm : ∀ {α : Type u} [c : comm_ring α] (a b : α), a * b = b * a
 44  comm_ring.add_assoc : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
 45  comm_ring.mul_assoc : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
 46  comm_ring.left_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
st       
 47  comm_ring.right_distrib : ∀ {α : Type u} [c : comm_ring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
 48  -/
 49  
 50  namespace CommRing.colimits
 51  
 52  variables {J : Type v} [small_category J] (F : J ⥤ CommRing.{v})
id                           └────────────┘            └──────┘
src                          └────────────┘            └──────┘
typ                          └────────────┘            └──────┘
doc                          └────────────┘            └──────┘
 53  
 54  inductive prequotient
 55  -- There's always `of`
 56  | of : Π (j : J) (x : F.obj j), prequotient
id                          └──┘ 
src                         └──┘
typ                         └──┘ 
 57  -- Then one generator for each operation
 58  | zero {} : prequotient
 59  | one {} : prequotient
 60  | neg : prequotient → prequotient
 61  | add : prequotient → prequotient → prequotient
 62  | mul : prequotient → prequotient → prequotient
 63  
 64  open prequotient
 65  
 66  inductive relation : prequotient F → prequotient F → Prop
id                        └─────────┘     └─────────┘
src                       └─────────┘     └─────────┘
typ                       └─────────┘     └─────────┘
 67  -- Make it an equivalence relation:
 68  | refl : Π (x), relation x x
id                            
typ                           
 69  | symm : Π (x y) (h : relation x y), relation y x
id                       └──────┘               
typ                      └──────┘               
 70  | trans : Π (x y z) (h : relation x y) (k : relation y z), relation x z
id                         └──────┘         └──────┘               
typ                        └──────┘         └──────┘               
 71  -- There's always a `map` relation
 72  | map : Π (j j' : J) (f : j ⟶ j') (x : F.obj j), relation (of j' (F.map f x)) (of j x)
id                               └┘        └──┘              └┘ └┘   └──┘      └┘  
src                                         └──┘               └┘      └──┘        └┘
typ                              └┘        └──┘              └┘ └┘   └──┘      └┘  
 73  -- Then one relation per operation, describing the interaction with `of`
 74  | zero : Π (j), relation (of j 0) zero
id                            └┘     └──┘
src                            └┘      └──┘
typ                           └┘     └──┘
 75  | one : Π (j), relation (of j 1) one
id                           └┘     └─┘
src                           └┘      └─┘
typ                          └┘     └─┘
 76  | neg : Π (j) (x : F.obj j), relation (of j (-x)) (neg (of j x))
id                      └──┘              └┘       └─┘  └┘  
src                      └──┘               └┘         └─┘  └┘
typ                     └──┘              └┘       └─┘  └┘  
 77  | add : Π (j) (x y : F.obj j), relation (of j (x + y)) (add (of j x) (of j y))
id                        └──┘              └┘         └─┘  └┘     └┘  
src                        └──┘               └┘            └─┘  └┘       └┘
typ                       └──┘              └┘         └─┘  └┘     └┘  
 78  | mul : Π (j) (x y : F.obj j), relation (of j (x * y)) (mul (of j x) (of j y))
id                        └──┘              └┘         └─┘  └┘     └┘  
src                        └──┘               └┘            └─┘  └┘       └┘
typ                       └──┘              └┘         └─┘  └┘     └┘  
 79  -- Then one relation per argument of each operation
 80  | neg_1 : Π (x x') (r : relation x x'), relation (neg x) (neg x')
id                 └┘       └──────┘  └┘             └─┘    └─┘ └┘
src                                                    └─┘     └─┘
typ                └┘       └──────┘  └┘             └─┘    └─┘ └┘
 81  | add_1 : Π (x x' y) (r : relation x x'), relation (add x y) (add x' y)
id                 └┘        └──────┘  └┘             └─┘     └─┘ └┘ 
src                                                      └─┘       └─┘
typ                └┘        └──────┘  └┘             └─┘     └─┘ └┘ 
 82  | add_2 : Π (x y y') (r : relation y y'), relation (add x y) (add x y')
id                  └┘       └──────┘  └┘             └─┘     └─┘  └┘
src                                                      └─┘       └─┘
typ                 └┘       └──────┘  └┘             └─┘     └─┘  └┘
 83  | mul_1 : Π (x x' y) (r : relation x x'), relation (mul x y) (mul x' y)
id                 └┘        └──────┘  └┘             └─┘     └─┘ └┘ 
src                                                      └─┘       └─┘
typ                └┘        └──────┘  └┘             └─┘     └─┘ └┘ 
 84  | mul_2 : Π (x y y') (r : relation y y'), relation (mul x y) (mul x y')
id                  └┘       └──────┘  └┘             └─┘     └─┘  └┘
src                                                      └─┘       └─┘
typ                 └┘       └──────┘  └┘             └─┘     └─┘  └┘
 85  -- And one relation per axiom
 86  | zero_add      : Π (x), relation (add zero x) x
id                                     └─┘ └──┘   
src                                     └─┘ └──┘
typ                                    └─┘ └──┘   
 87  | add_zero      : Π (x), relation (add x zero) x
id                                     └─┘  └──┘  
src                                     └─┘   └──┘
typ                                    └─┘  └──┘  
 88  | one_mul       : Π (x), relation (mul one x) x
id                                     └─┘ └─┘   
src                                     └─┘ └─┘
typ                                    └─┘ └─┘   
 89  | mul_one       : Π (x), relation (mul x one) x
id                                     └─┘  └─┘  
src                                     └─┘   └─┘
typ                                    └─┘  └─┘  
 90  | add_left_neg  : Π (x), relation (add (neg x) x) zero
id                                     └─┘  └─┘     └──┘
src                                     └─┘  └─┘       └──┘
typ                                    └─┘  └─┘     └──┘
 91  | add_comm      : Π (x y), relation (add x y) (add y x)
id                                      └─┘     └─┘  
src                                       └─┘       └─┘
typ                                     └─┘     └─┘  
 92  | mul_comm      : Π (x y), relation (mul x y) (mul y x)
id                                      └─┘     └─┘  
src                                       └─┘       └─┘
typ                                     └─┘     └─┘  
 93  | add_assoc     : Π (x y z), relation (add (add x y) z) (add x (add y z))
id                                       └─┘  └─┘       └─┘   └─┘  
src                                         └─┘  └─┘          └─┘    └─┘
typ                                      └─┘  └─┘       └─┘   └─┘  
 94  | mul_assoc     : Π (x y z), relation (mul (mul x y) z) (mul x (mul y z))
id                                       └─┘  └─┘       └─┘   └─┘  
src                                         └─┘  └─┘          └─┘    └─┘
typ                                      └─┘  └─┘       └─┘   └─┘  
 95  | left_distrib  : Π (x y z), relation (mul x (add y z)) (add (mul x y) (mul x z))
id                                       └─┘   └─┘      └─┘  └─┘     └─┘  
src                                         └─┘    └─┘        └─┘  └─┘       └─┘
typ                                      └─┘   └─┘      └─┘  └─┘     └─┘  
 96  | right_distrib : Π (x y z), relation (mul (add x y) z) (add (mul x z) (mul y z))
id                                       └─┘  └─┘       └─┘  └─┘     └─┘  
src                                         └─┘  └─┘          └─┘  └─┘       └─┘
typ                                      └─┘  └─┘       └─┘  └─┘     └─┘  
 97  
 98  def colimit_setoid : setoid (prequotient F) :=
id                        └────┘  └─────────┘ 
src                       └────┘  └─────────┘
typ                       └────┘  └─────────┘ 
 99  { r := relation F, iseqv := ⟨relation.refl, relation.symm, relation.trans⟩ }
id          └──────┘             └───────────┘  └───────────┘  └────────────┘
src         └──────┘              └───────────┘  └───────────┘  └────────────┘
typ         └──────┘             └───────────┘  └───────────┘  └────────────┘
100  attribute [instance] colimit_setoid
id                        └────────────┘
src                       └────────────┘
typ                       └────────────┘
101  
102  def colimit_type : Type v := quotient (colimit_setoid F)
id                                └──────┘  └────────────┘ 
src                               └──────┘  └────────────┘
typ                               └──────┘  └────────────┘ 
103  
104  instance : comm_ring (colimit_type F) :=
id              └───────┘  └──────────┘ 
src             └───────┘  └──────────┘
typ             └───────┘  └──────────┘ 
105  { zero :=
106    begin
st     └─────
107      exact quot.mk _ zero
id             └─────┘   └──┘
src      └────┘       └─┘└──┘
typ      └────┘└─────┘└─┘└──┘
doc      └────┘       └─┘    
txt      └────┘       └─┘    
par      └────┘       └─┘    
pid                  └─┘    
st   ─────────────────────────
108    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
109    one :=
110    begin
st     └─────
111      exact quot.mk _ one
id             └─────┘   └─┘
src      └────┘       └─┘└─┘
typ      └────┘└─────┘└─┘└─┘
doc      └────┘       └─┘   
txt      └────┘       └─┘   
par      └────┘       └─┘   
pid                  └─┘   
st   ────────────────────────
112    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
113    neg :=
114    begin
st     └─────
115      fapply @quot.lift,
id               └───────┘
src      └─────┘
typ      └─────┘ └───────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid            
st   ────────────────────┘└─
116      { intro x,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid             └┘
st   ─────┘└─────┘└─
117        exact quot.mk _ (neg x) },
id               └─────┘    └─┘ 
src        └────┘       └─┘ └─┘ └┘
typ        └────┘└─────┘└─┘ └─┘└┘
doc        └────┘       └─┘     └┘
txt        └────┘       └─┘     └┘
par        └────┘       └─┘     └┘
pid                    └─┘     
st   ─────────────────────────────┘└┘
118      { intros x x' r,
src        └───────────┘
typ        └───────────┘
doc        └───────────┘
txt        └───────────┘
par        └───────────┘
pid              └─────┘
st   ──────────────────┘└─
119        apply quot.sound,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
120        exact relation.neg_1 _ _ r },
id               └────────────┘     
src        └────┘└────────────┘└───┘ 
typ        └────┘└────────────┘└───┘
doc        └────┘              └───┘ 
txt        └────┘              └───┘ 
par        └────┘              └───┘ 
pid                           └───┘ 
st   ────────────────────────────────┘└──
121    end,
st   ────┘
122    add :=
123    begin
st     └─────
124      fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
id               └───────┘       └──────────┘       └──────────┘ 
src      └─────┘          └───┘               └┘  └──────────┘ └┘
typ      └─────┘ └───────┘└───┘  └──────────┘ └┘  └──────────┘└┘
doc      └─────┘          └───┘               └┘               └┘
txt      └─────┘          └───┘               └┘               └┘
par      └─────┘          └───┘               └┘               └┘
pid                      └───┘               └┘               └┘
st   ──────────────────────────────────────────────────────────────┘└─
125      { intro x,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid             └┘
st   ─────┘└─────┘└─
126        fapply @quot.lift,
id                 └───────┘
src        └─────┘
typ        └─────┘ └───────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid              
st   ──────────────────────┘└─
127        { intro y,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
pid               └┘
st   ───────┘└─────┘└─
128          exact quot.mk _ (add x y) },
id                 └─────┘    └─┘  
src          └────┘       └─┘ └─┘  └┘
typ          └────┘└─────┘└─┘ └─┘└┘
doc          └────┘       └─┘      └┘
txt          └────┘       └─┘      └┘
par          └────┘       └─┘      └┘
pid                      └─┘      
st   ─────────────────────────────────┘└┘
129        { intros y y' r,
src          └───────────┘
typ          └───────────┘
doc          └───────────┘
txt          └───────────┘
par          └───────────┘
pid                └─────┘
st   ────────────────────┘└─
130          apply quot.sound,
id                 └────────┘
src          └────┘└────────┘
typ          └────┘└────────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────────────────────┘└─
131          exact relation.add_2 _ _ _ r } },
id                 └────────────┘       
src          └────┘└────────────┘└─────┘ 
typ          └────┘└────────────┘└─────┘
doc          └────┘              └─────┘ 
txt          └────┘              └─────┘ 
par          └────┘              └─────┘ 
pid                             └─────┘ 
st   ────────────────────────────────────┘└──┘
132      { intros x x' r,
src        └───────────┘
typ        └───────────┘
doc        └───────────┘
txt        └───────────┘
par        └───────────┘
pid              └─────┘
st   ──────────────────┘└─
133        funext y,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid              └┘
st   ─────────────┘└─
134        induction y,
id                   
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid                 
st   ────────────────┘└─
135        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
136        apply quot.sound,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
137        { exact relation.add_1 _ _ _ r },
id                 └────────────┘       
src          └────┘└────────────┘└─────┘ 
typ          └────┘└────────────┘└─────┘
doc          └────┘              └─────┘ 
txt          └────┘              └─────┘ 
par          └────┘              └─────┘ 
pid                             └─────┘ 
st   ───────┘└───────────────────────────┘└┘
138        { refl } },
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
pid              
st   ────────────┘└────
139    end,
st   ────┘
140    mul :=
141    begin
st     └─────
142      fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
id               └───────┘                          └──────────┘ 
src      └─────┘          └───┘               └┘  └──────────┘ └┘
typ      └─────┘ └───────┘└───┘               └┘  └──────────┘└┘
doc      └─────┘          └───┘               └┘               └┘
txt      └─────┘          └───┘               └┘               └┘
par      └─────┘          └───┘               └┘               └┘
pid                      └───┘               └┘               └┘
st   ──────────────────────────────────────────────────────────────┘└─
143      { intro x,
src        └─────┘
typ        └─────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid             └┘
st   ─────┘└─────┘└─
144        fapply @quot.lift,
id                 └───────┘
src        └─────┘
typ        └─────┘ └───────┘
doc        └─────┘
txt        └─────┘
par        └─────┘
pid              
st   ──────────────────────┘└─
145        { intro y,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
pid               └┘
st   ───────┘└─────┘└─
146          exact quot.mk _ (mul x y) },
id                 └─────┘    └─┘  
src          └────┘       └─┘ └─┘  └┘
typ          └────┘└─────┘└─┘ └─┘└┘
doc          └────┘       └─┘      └┘
txt          └────┘       └─┘      └┘
par          └────┘       └─┘      └┘
pid                      └─┘      
st   ─────────────────────────────────┘└┘
147        { intros y y' r,
src          └───────────┘
typ          └───────────┘
doc          └───────────┘
txt          └───────────┘
par          └───────────┘
pid                └─────┘
st   ────────────────────┘└─
148          apply quot.sound,
id                 └────────┘
src          └────┘└────────┘
typ          └────┘└────────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────────────────────┘└─
149          exact relation.mul_2 _ _ _ r } },
id                 └────────────┘       
src          └────┘└────────────┘└─────┘ 
typ          └────┘└────────────┘└─────┘
doc          └────┘              └─────┘ 
txt          └────┘              └─────┘ 
par          └────┘              └─────┘ 
pid                             └─────┘ 
st   ────────────────────────────────────┘└──┘
150      { intros x x' r,
src        └───────────┘
typ        └───────────┘
doc        └───────────┘
txt        └───────────┘
par        └───────────┘
pid              └─────┘
st   ──────────────────┘└─
151        funext y,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid              └┘
st   ─────────────┘└─
152        induction y,
id                   
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid                 
st   ────────────────┘└─
153        dsimp,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
154        apply quot.sound,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
155        { exact relation.mul_1 _ _ _ r },
id                 └────────────┘       
src          └────┘└────────────┘└─────┘ 
typ          └────┘└────────────┘└─────┘
doc          └────┘              └─────┘ 
txt          └────┘              └─────┘ 
par          └────┘              └─────┘ 
pid                             └─────┘ 
st   ───────┘└───────────────────────────┘└┘
156        { refl } },
src          └───┘
typ          └───┘
doc          └───┘
txt          └───┘
par          └───┘
pid              
st   ────────────┘└────
157    end,
st   ────┘
158    zero_add := λ x,
id                   
typ                  
159    begin
st     └─────
160      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
161      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
162      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
163      apply relation.zero_add,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
164      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
165    end,
st   ────┘
166    add_zero := λ x,
id                   
typ                  
167    begin
st     └─────
168      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
169      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
170      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
171      apply relation.add_zero,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
172      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
173    end,
st   ────┘
174    one_mul := λ x,
id                  
typ                 
175    begin
st     └─────
176      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
177      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
178      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
179      apply relation.one_mul,
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────┘└─
180      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
181    end,
st   ────┘
182    mul_one := λ x,
id                  
typ                 
183    begin
st     └─────
184      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
185      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
186      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
187      apply relation.mul_one,
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────────────────┘└─
188      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
189    end,
st   ────┘
190    add_left_neg := λ x,
id                       
typ                      
191    begin
st     └─────
192      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
193      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
194      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
195      apply relation.add_left_neg,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
196      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
197    end,
st   ────┘
198    add_comm := λ x y,
id                    
typ                   
199    begin
st     └─────
200      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
201      induction y,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
202      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
203      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
204      apply relation.add_comm,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
205      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
206      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
207    end,
st   ────┘
208    mul_comm := λ x y,
id                    
typ                   
209    begin
st     └─────
210      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
211      induction y,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
212      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
213      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
214      apply relation.mul_comm,
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
215      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
216      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
217    end,
st   ────┘
218    add_assoc := λ x y z,
id                      
typ                     
219    begin
st     └─────
220      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
221      induction y,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
222      induction z,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
223      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
224      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
225      apply relation.add_assoc,
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────────┘└─
226      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
227      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
228      refl,
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
st   ───────┘└─
229    end,
st   ────┘
230    mul_assoc := λ x y z,
id                      
typ                     
231    begin
st     └─────
232      induction x,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
233      induction y,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
234      induction z,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
235      dsimp,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
236      apply quot.sound,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
237      apply relation.mul_assoc,
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────────────┘
238      refl,
239      refl,
240      refl,
st           └─
241    end,
st   ────┘
242    left_distrib := λ x y z,
id                         
typ                        
243    begin
244      induction x,
245      induction y,
246      induction z,
247      dsimp,
248      apply quot.sound,
249      apply relation.left_distrib,
250      refl,
251      refl,
252      refl,
st           └─
253    end,
st   ────┘
254    right_distrib := λ x y z,
id                          
typ                         
255    begin
256      induction x,
257      induction y,
258      induction z,
259      dsimp,
260      apply quot.sound,
261      apply relation.right_distrib,
262      refl,
263      refl,
264      refl,
st           └─
265    end, }
st   ────┘
266  
267  @[simp] lemma quot_zero : quot.mk setoid.r zero = (0 : colimit_type F) := rfl
id                             └─────┘ └──────┘ └──┘       └──────────┘      └─┘
src                                    └──────┘ └──┘       └──────────┘       └─┘
typ                            └─────┘ └──────┘ └──┘       └──────────┘      └─┘
doc    └──┘
268  @[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl
id                            └─────┘ └──────┘ └─┘       └──────────┘      └─┘
src                                   └──────┘ └─┘       └──────────┘       └─┘
typ                           └─────┘ └──────┘ └─┘       └──────────┘      └─┘
doc    └──┘
269  @[simp] lemma quot_neg (x) : quot.mk setoid.r (neg x) = (-(quot.mk setoid.r x) : colimit_type F) := rfl
id                                └─────┘ └──────┘  └─┘      └─────┘ └──────┘     └──────────┘      └─┘
src                                       └──────┘  └─┘               └──────┘      └──────────┘       └─┘
typ                               └─────┘ └──────┘  └─┘      └─────┘ └──────┘     └──────────┘      └─┘
doc    └──┘
270  @[simp] lemma quot_add (x y) : quot.mk setoid.r (add x y) = ((quot.mk setoid.r x) + (quot.mk setoid.r y) : colimit_type F) := rfl
id                                  └─────┘ └──────┘  └─┘       └─────┘ └──────┘     └─────┘ └──────┘     └──────────┘      └─┘
src                                         └──────┘  └─┘                 └──────┘              └──────┘      └──────────┘       └─┘
typ                                 └─────┘ └──────┘  └─┘       └─────┘ └──────┘     └─────┘ └──────┘     └──────────┘      └─┘
doc    └──┘
271  @[simp] lemma quot_mul (x y) : quot.mk setoid.r (mul x y) = ((quot.mk setoid.r x) * (quot.mk setoid.r y) : colimit_type F) := rfl
id                                  └─────┘ └──────┘  └─┘       └─────┘ └──────┘     └─────┘ └──────┘     └──────────┘      └─┘
src                                         └──────┘  └─┘                 └──────┘              └──────┘      └──────────┘       └─┘
typ                                 └─────┘ └──────┘  └─┘       └─────┘ └──────┘     └─────┘ └──────┘     └──────────┘      └─┘
doc    └──┘
272  
273  def colimit : CommRing := CommRing.of (colimit_type F)
id                 └──────┘    └─────────┘  └──────────┘ 
src                └──────┘    └─────────┘  └──────────┘
typ                └──────┘    └─────────┘  └──────────┘ 
doc                └──────┘    └─────────┘
274  
275  def cocone_fun (j : J) (x : F.obj j) : colimit_type F :=
id                              └──┘     └──────────┘ 
src                               └──┘      └──────────┘
typ                             └──┘     └──────────┘ 
276  quot.mk _ (of j x)
id   └─────┘    └┘  
src             └┘
typ  └─────┘    └┘  
277  
278  def cocone_morphism (j : J) : F.obj j ⟶ colimit F :=
id                                └──┘   └─────┘ 
src                                 └──┘    └─────┘
typ                               └──┘   └─────┘ 
279  { to_fun := cocone_fun F j,
id               └────────┘  
src              └────────┘
typ              └────────┘  
280    map_one' := by apply quot.sound; apply relation.one,
id                          └────────┘        └──────────┘
src                   └────┘└────────┘  └────┘└──────────┘
typ                   └────┘└────────┘  └────┘└──────────┘
doc                   └────┘            └────┘
txt                   └────┘            └────┘
par                   └────┘            └────┘
pid                                         
st                   └───────────────────────────────────┘
281    map_mul' := by intros; apply quot.sound; apply relation.mul,
id                                  └────────┘        └──────────┘
src                   └────┘  └────┘└────────┘  └────┘└──────────┘
typ                   └────┘  └────┘└────────┘  └────┘└──────────┘
doc                   └────┘  └────┘            └────┘
txt                   └────┘  └────┘            └────┘
par                   └────┘  └────┘            └────┘
pid                                                 
st                   └───────────────────────────────────────────┘
282    map_zero' := by apply quot.sound; apply relation.zero,
id                           └────────┘        └───────────┘
src                    └────┘└────────┘  └────┘└───────────┘
typ                    └────┘└────────┘  └────┘└───────────┘
doc                    └────┘            └────┘
txt                    └────┘            └────┘
par                    └────┘            └────┘
pid                                          
st                    └────────────────────────────────────┘
283    map_add' := by intros; apply quot.sound; apply relation.add }
id                                  └────────┘        └──────────┘
src                   └────┘  └────┘└────────┘  └────┘└──────────┘
typ                   └────┘  └────┘└────────┘  └────┘└──────────┘
doc                   └────┘  └────┘            └────┘            
txt                   └────┘  └────┘            └────┘            
par                   └────┘  └────┘            └────┘            
pid                                                             
st                   └────────────────────────────────────────────┘
284  
285  @[simp] lemma cocone_naturality {j j' : J} (f : j ⟶ j') :
id                                                    └┘
src                                                    
typ                                                   └┘
doc    └──┘
286    F.map f ≫ (cocone_morphism F j') = cocone_morphism F j :=
id     └──┘    └─────────────┘  └┘   └─────────────┘  
src     └──┘     └─────────────┘        └─────────────┘
typ    └──┘    └─────────────┘  └┘   └─────────────┘  
287  begin
st   └─────
288    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
289    apply quot.sound,
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────┘└─
290    apply relation.map,
id           └──────────┘
src    └────┘└──────────┘
typ    └────┘└──────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────┘└─
291  end
st   ──┘
292  
293  @[simp] lemma cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j):
id                                                               └┘       └──┘ 
src                                                                          └──┘
typ                                                              └┘       └──┘ 
doc    └──┘
294    (cocone_morphism F j') (F.map f x) = (cocone_morphism F j) x :=
id      └─────────────┘  └┘   └──┘      └─────────────┘    
src     └─────────────┘         └──┘        └─────────────┘
typ     └─────────────┘  └┘   └──┘      └─────────────┘    
295  by { rw ←cocone_naturality F f, refl }
id            └───────────────┘  
src       └──┘└───────────────┘    
typ       └──┘└───────────────┘  
doc       └──┘                     
txt       └──┘                     
par       └──┘                     
pid         └┘                  
st       └───────────────────────┘ └┘    └┘
296  
297  def colimit_cocone : cocone F :=
298  { X := colimit F,
299    ι :=
300    { app := cocone_morphism F } }.
id     
src    
typ    
doc    
301  
302  @[simp] def desc_fun_lift (s : cocone F) : prequotient F → s.X
doc    └──┘
303  | (of j x)  := (s.ι.app j) x
id         
typ        
304  | zero      := 0
305  | one       := 1
306  | (neg x)   := -(desc_fun_lift x)
id          
typ         
307  | (add x y) := desc_fun_lift x + desc_fun_lift y
id           
typ          
308  | (mul x y) := desc_fun_lift x * desc_fun_lift y
id           
typ          
309  
310  def desc_fun (s : cocone F) : colimit_type F → s.X :=
311  begin
312    fapply quot.lift,
313    { exact desc_fun_lift F s },
st                               └┘
314    { intros x y r,
315      induction r; try { dsimp },
id                    └─┘
src                   └─┘
typ                   └─┘
doc                   └─┘
316      -- refl
317      { refl },
st              └┘
318      -- symm
319      { exact r_ih.symm },
st                         └┘
320      -- trans
321      { exact eq.trans r_ih_h r_ih_k },
st                                      └┘
322      -- map
323      { rw cocone.naturality_concrete, },
st                                        └┘
324      -- zero
325      { erw is_ring_hom.map_zero ⇑((s.ι).app r), refl },
id                                              
typ                                             
st                                                       └┘
326      -- one
327      { erw is_ring_hom.map_one ⇑((s.ι).app r), refl },
id                                             
typ                                            
st                                                      └┘
328      -- neg
329      { rw is_ring_hom.map_neg ⇑((s.ι).app r_j) },
id                                            └─┘
typ                                           └─┘
st                                                 └┘
330      -- add
331      { rw is_ring_hom.map_add ⇑((s.ι).app r_j) },
id                                            └─┘
typ                                           └─┘
st                                                 └┘
332      -- mul
333      { rw is_ring_hom.map_mul ⇑((s.ι).app r_j) },
id                                            └─┘
typ                                           └─┘
st                                                 └┘
334      -- neg_1
335      { rw r_ih, },
st                  └┘
336      -- add_1
337      { rw r_ih, },
st                  └┘
338      -- add_2
339      { rw r_ih, },
st                  └┘
340      -- mul_1
341      { rw r_ih, },
st                  └┘
342      -- mul_2
343      { rw r_ih, },
st                  └┘
344      -- zero_add
345      { rw zero_add, },
st                      └┘
346      -- add_zero
347      { rw add_zero, },
st                      └┘
348      -- one_mul
349      { rw one_mul, },
st                     └┘
350      -- mul_one
351      { rw mul_one, },
st                     └┘
352      -- add_left_neg
353      { rw add_left_neg, },
st                          └┘
354      -- add_comm
355      { rw add_comm, },
st                      └┘
356      -- mul_comm
357      { rw mul_comm, },
st                      └┘
358      -- add_assoc
359      { rw add_assoc, },
st                       └┘
360      -- mul_assoc
361      { rw mul_assoc, },
st                       └┘
362      -- left_distrib
363      { rw left_distrib, },
st                          └┘
364      -- right_distrib
365      { rw right_distrib, },
st                           └┘
366    }
st     └─
367  end
st   ──┘
368  
369  @[simp] def desc_morphism (s : cocone F) : colimit F ⟶ s.X :=
doc    └──┘
370  { to_fun := desc_fun F s,
371    map_one' := rfl,
372    map_zero' := rfl,
373    map_add' := λ x y, by { induction x; induction y; refl },
id                                                       └──┘
src                                                      └──┘
typ                                                      └──┘
doc                                                      └──┘
st                                                            └┘
374    map_mul' := λ x y, by { induction x; induction y; refl }, }
id                                                       └──┘
src                                                      └──┘
typ                                                      └──┘
doc                                                      └──┘
st                                                            └┘
375  
376  def colimit_is_colimit : is_colimit (colimit_cocone F) :=
377  { desc := λ s, desc_morphism F s,
id   
src  
typ  
doc  
378    uniq' := λ s m w,
379    begin
380      ext,
381      induction x,
382      induction x,
id                 
typ                
383      { have w' := congr_fun (congr_arg (λ f : F.obj x_j ⟶ s.X, (f : F.obj x_j → s.X)) (w x_j)) x_x,
id                                                                                           └─┘
typ                                                                                          └─┘
384        erw w',
385        refl, },
st               └┘
386      { simp only [desc_morphism, quot_zero],
387        erw is_ring_hom.map_zero ⇑m,
388        refl, },
st               └┘
389      { simp only [desc_morphism, quot_one],
390        erw is_ring_hom.map_one ⇑m,
391        refl, },
st               └┘
392      { simp only [desc_morphism, quot_neg],
393        erw is_ring_hom.map_neg ⇑m,
394        rw [x_ih],
395        refl, },
st               └┘
396      { simp only [desc_morphism, quot_add],
397        erw is_ring_hom.map_add ⇑m,
398        rw [x_ih_a, x_ih_a_1],
399        refl, },
st               └┘
400      { simp only [desc_morphism, quot_mul],
401        erw is_ring_hom.map_mul ⇑m,
402        rw [x_ih_a, x_ih_a_1],
403        refl, },
st               └┘
404      refl
405    end }.
st     └─┘
406  
407  instance has_colimits_CommRing : has_colimits.{v} CommRing.{v} :=
id                                                     └──┘  └┘
src                                                    └──┘  └┘
typ                                                    └──┘  └┘
doc                                                    └──┘  └┘
408  { has_colimits_of_shape := λ J 𝒥,
id                                 
typ                                
409    { has_colimit := λ F, by exactI
410      { cocone := colimit_cocone F,
411        is_colimit := colimit_is_colimit F } } }
412  
413  end CommRing.colimits